| Definitions | t  T, s = t, x:A  B(x),  x:A. B(x), E(X), ES, Type, AbsInterface(A), sys-antecedent(es;Sys), chain-consistent(f;chain), y is f*(x),  , <a, b>, E, type List, x:A  B(x),  x:A. B(x), P   Q,  b, left + right, {x:A| B(x)} , Id, P  Q, a < b,  A, P & Q, hd(l), L1  L2, e  loc e' , adjacent(T;L;x;y), (x l), no_repeats(T;l), y=f*(x) via L, False, Top, f(a), loc(e), x <<= y, x << y, X(e), e  X,  , let x,y = A in B(x;y), t.1, a:A fp B(a), strong-subtype(A;B), case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , (e <loc e'), Unit, ff, inr x , tt, inl x , True, A c B, Atom$n, x before y l, e c e', !Void(), f**(e),  , l[i], {T}, source(l), destination(l), es-init(es;e), P  Q, P Q, isrcv(e), kind(e), es-first-from(es;e;l;tg), isrcv(k), lastchange(x;e), (last change to x before e), last(L), {i..j },  , x dom(f), EqDecider(T), IdLnk, EOrderAxioms(E; pred?; info), EState(T), Knd,   x. t(x), x,y. t(x;y), kindcase(k; a.f(a); l,t.g(l;t) ), Msg(M), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), e < e', r s, constant_function(f;A;B), f(x)?z,  T |
